Report for no_context/loop4.c

1

extern void abort(void);  

2

extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));  

3

void reach_error() { __assert_fail("0", "loop4.c", 10, "reach_error"); }  

4

void assume_abort_if_not(int cond) {  

5

  if(!cond) {abort();}  

6

}  

7

void __VERIFIER_assert(int cond) { if(!(cond)) { ERROR: {reach_error();abort();} } }  

8

extern int __VERIFIER_nondet_int(void);  

9

extern void __VERIFIER_assume(int);  

10

11

int main() {  

12

    int x,y;  

13

    x = 0;  

14

    y = 0;  

15

    while (1) {  

16

        if (x < 50) {  

17

            y++;  

18

        } else {  

19

            y--;  

20

        }  

21

        if (y < 0) break;  

22

        x++;  

23

    }  

24

    __VERIFIER_assert(x == 100);  

25

    return 0;  

26

}